$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$), $P$:($T$$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$x$, $y$:$T$. Dec($R$($x$,$y$)))
\\[0ex]$\Rightarrow$ ($\forall$$x$:$T$. Dec($P$($x$)))
\\[0ex]$\Rightarrow$ ($\forall$$y$:$T$. $\exists$$L$:$T$ List. ($\forall$$x$:$T$. ($R$($x$,$y$)) $\Rightarrow$ ($x$ $\in$ $L$)))
\\[0ex]$\Rightarrow$ WellFnd\{i\}($T$;$x$,$y$.$R$($x$,$y$))
\\[0ex]$\Rightarrow$ ($\forall$$z$:$T$. ($P$($z$)) $\Rightarrow$ ($\exists$$y$:$T$. ($P$($y$) \& ($R$$^{\mbox{\scriptsize $\ast$}}$)($y$,$z$) \& ($\forall$$x$:$T$. ($R$\^{}+($x$,$y$)) $\Rightarrow$ ($\neg$($P$($x$)))))))